\begin{tabbing}
when{-}after($e$;${\it info}$;${\it pred?}$;${\it init}$;${\it Trans}$;${\it val}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if \=first(${\it pred?}$;$e$)$\rightarrow$\+\+
\\[0ex]$\langle$$\lambda$$x$.${\it init}$(loc(${\it info}$;$e$),$x$)
\\[0ex]$,\,$${\it Trans}$(loc(${\it info}$;$e$),kind(${\it info}$;$e$),${\it val}$($e$),$\lambda$$x$.${\it init}$(loc(${\it info}$;$e$),$x$))$\rangle$
\-\\[0ex]else \=let $p$ = when{-}after(pred(${\it pred?}$;$e$);${\it info}$;${\it pred?}$;${\it init}$;${\it Trans}$;${\it val}$) in \+
\\[0ex]$\langle$2of($p$)$,\,$${\it Trans}$(loc(${\it info}$;$e$),kind(${\it info}$;$e$),${\it val}$($e$),2of($p$))$\rangle$ fi
\-\-\\[0ex]\emph{(recursive)}
\end{tabbing}